detach\_fun($T$;$A$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{$d$:$T$$\rightarrow\mathbb{B}\mid$ $\forall$$x$:$T$. ($\downarrow$($A$($x$))) $\Leftarrow\!\Rightarrow$ ($\uparrow$($d$($x$)))\}